 $LOAD_PATH.unshift File.join(File.dirname(__FILE__),'../..','ext_pr1/lib')
 require 'ext_pr1_v4'

 module Clock_Const
MIN_IN_SEC = 60
HOUR_IN_MIN = 60
DAY_IN_HOUR = 24
HOUR_IN_SEC = HOUR_IN_MIN * MIN_IN_SEC
DAY_IN_SEC = DAY_IN_HOUR * HOUR_IN_SEC
HALF_DAY_IN_SEC = DAY_IN_SEC / 2
HALF_DAY = DAY_IN_HOUR/2
 end

 # Die Klasse Objekt die alle Fälle als FALSE implementiert hat
 
class Object
 def day_sec?() false end
 def hour24?() false end
 def hour12?() false end
 def halve?() false end
 def min?() false end
 def sec?() false end
 def clock_sec?() false end
 def clock_24?() false end
 def clock_12?() false end
end
  
# Die Klassen für die Einzelfälle
# Überprüfung auf day_sec?
class Integer
 include Clock_Const
 def day_sec?() self.int? and self.in?(0...DAY_IN_SEC) end
#Überprüfung auf hour24?
 def hour24?() self.int? and self.in?(0...DAY_IN_HOUR) end
#Überprüfung auf hour12?
 def hour12?() self.int? and self.in?(0...(HALF_DAY)) end
#Überprüfung auf min
 def min?() self.int? and self.in?(0...HOUR_IN_MIN) end
#Überprüfung auf sec
 def sec?() self.int? and self.in?(0...MIN_IN_SEC) end
end

class Clock
 include Clock_Const
  def clock?() self.clock_sec? or self.clock_24? or self.clock_12? end
  def day_sec() to_clock_sec().day_sec end
  def sec() to_clock_12().sec end
  def min() to_clock_12().min end
  def hour24() to_clock_24().hour24 end
  def hour12() to_clock_12().hour12 end
  def halve() to_clock_12().halve end
  def ==(o) self.equal?(o) or (o.clock? and (day_sec == o.day_sec)) end
  def to_clock_sec() abstract end
  def from() abstract end
  def to_clock_12() abstract end
  def to_clock_24() abstract end
  def add(o) 
    self.from(ClockSec[self.to_clock_sec.day_sec + o.to_clock_sec.day_sec])
  end
    alias :+ :add
  def clock_sub(o) 
    self.from(ClockSec[self.to_clock_sec.day_sec - o.to_clock_sec.day_sec])
  end
    alias :- :clock_sub
  def clock_pred() abstract end
  def clock_succ() abstract end
  def invers() abstract end
  def zero() abstract end
 
end

class ClockSec < Clock
  
  def initialize(day_sec) @day_sec = day_sec end
  
  def self.[](*args) check_inv(self.new(*args)) end
  
  def invariant?() day_sec.day_sec? end
  
  def to_clock_sec() self end
  def day_sec() @day_sec end
  def clock_sec?() true end
  
  def clock_succ() ClockSec[day_sec.succ()] end
  def clock_pred() ClockSec[day_sec.pred()] end
  
  def to_clock_24()
    hour24, hour_carry = day_sec.divmod(HOUR_IN_SEC)
    min, sec = hour_carry.divmod(MIN_IN_SEC)
    Clock24[hour24, min, sec]
  end
  
  def to_clock_12()
    clock24 = self.to_clock_24
    halve = (clock24.hour24 / HALF_DAY) == 1 ? :PM : :AM
    hour = clock24.hour24 > HALF_DAY ? clock24.hour24 - HALF_DAY : clock24.hour24
    Clock12[halve, hour, clock24.min, clock24.sec]
  end
  
  def invers() ClockSec[to_clock_sec().day_sec - DAY_IN_SEC] end
  
  def zero() ClockSec[to_clock_sec().day_sec = 0] end
  
  def from(clock)
    check_pre((clock.clock?))
    clock.to_clock_sec
  end
  
  def to_s() 'ClockSec'+'['+(day_sec.to_s)+']' end
end
class Clock24 < Clock
  ######################Initialize#######################################
  def initialize(hour24, min, sec)
    @hour24 = hour24
    @min = min
    @sec = sec
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
  
  def invariant?() @hour24.hour24? and @min.min? and @sec.sec? end
  #####################Typprädikat######################################
  def clock_24?() true end
  #####################Selektoren#######################################
  def hour24() @hour24 end
  def min() @min end
  def sec() @sec end
  ####################Konversionen######################################
  def to_clock_24() self end
  def to_clock_12() to_clock_sec().to_clock_12() end
  def to_clock_sec() ClockSec[(@hour24 * HOUR_IN_SEC) + (@min * MIN_IN_SEC) + @sec] end
  
  def from(clock)
    check_pre((clock.clock?))
    clock.to_clock_24()
  end
  def to_s() 'Clock24'+'['+(hour24.to_s)+","+(min.to_s)+","+(sec.to_s)+']' end 
  #########################Operatoren###################################
  def clock_pred() to_clock_sec().clock_pred().to_clock_24() end
  def clock_succ() to_clock_sec().clock_sec_succ().to_clock_24() end
  def invers() ClockSec[to_clock_sec().day_sec - DAY_IN_SEC].to_clock_24 end
  def zero() Clock24[to_clock_sec().day_sec = 0].to_clock_24() end
end

class Clock12 < Clock
  
  ########################Initialize########################
  def initialize(halve, hour12, min, sec)
    @halve = halve
    @hour12 = hour12
    @min = min
    @sec = sec
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
  
  def invariant?() self.halve? and @hour12.hour12? and @min.min? and @sec.sec? end
  
  ###################Typprädikate###########################
  def halve?() @halve == :AM or @halve == :PM end
  def clock_12?() true end
 #######################Selektoren##########################
 def sec() @sec end
 def min() @min end
 def hour12() @hour12 end
 def halve() @halve end
##################Konversionen############################### 
  def to_clock_sec() ClockSec[(@halve == :AM ? (@hour12 * HOUR_IN_SEC) : ((@hour12 + HALF_DAY) * HOUR_IN_SEC)) + (@min * MIN_IN_SEC) + @sec] end
  def to_clock_24() to_clock_sec().to_clock_24() end
  def to_clock_12() self end
  def to_s() 'Clock12'+'['+(halve.to_s)+","+(hour12.to_s)+","+(min.to_s)+","+(sec.to_s)+']' end 
####################Operatoren###############################
  def clock_pred() to_clock_sec.clock_pred.to_clock_12 end
  def clock_succ() to_clock_sec.succ.to_clock_12 end
  def invers() ClockSec[to_clock_sec().day_sec - DAY_IN_SEC].to_clock_12 end
  def zero() Clock12[to_clock_sec().day_sec = 0].to_clock_12() end
end